T:Type, l:(T List), a,x,y:T.
l_before(x; y; cons(a; l); T)  (((x = a)  (y  l))  l_before(x; y; l; T)) 

latex

Definitions	P  Q, P  Q, P  Q, P  Q, P  Q, x:A. B(x), prop{i:l}, t  T
Lemmas	l member wf, sublist wf, iff wf